00100	GIVEAX(SCORDERING,(∀ R)(SCORDERING R ≡ ORDERING R ∧
00200		UUεDOMAIN R
00300	∧	(∀ X)(XεDOMAIN R ⊃ ββ(UU,R,X))
00400	∧	(∀ S)(ASCENDSEQ(R,S) ⊃
00500			LUB(R,S)εDOMAIN R
00600		∧	(∀ X)(XεRRANGE S ⊃ ββ(X,R,LUB(R,S)))
00700		∧	(∀ U)((∀ X)(XεRRANGE S ⊃ ββ(X,R,U))
00800				⊃ββ(LUB(R,S),R,U)))));
00900	
01000	GIVEAX(SCFUNS1,(∀ R1)(∀ R2)(SCORDERING R1 ∧ SCORDERING R2
01100		⊃ (∀ F)(FεDOMAIN(R1→→R2) 
01200			≡ Fε(DOMAIN R1 → DOMAIN R2)
01300				∧ CONTINUOUS(F,R1,R2))));
01400	
01500	GIVEAX(SCFUNS2,(∀ R1)(∀ R2)(SCORDERING R1 ∧ SCORDERING R2
01600		⊃ SCORDERING(R1→→R2) ∧ (∀ F)(F ε DOMAIN(R1→→R2) ≡
01700			CONTINUOUS(F,R1,R2))));
01800	
01900	GIVEAX(SCTV1,SCORDERING RTV);
02000	
02100	GIVEAX(SCTV2,SCTV = DOMAIN RTV);
02200	
02300	GIVEAX(SCTV3,(∀ X)(XεSCTV ≡ X=T ∨ X=F ∨ X=UU));
02400	
02500	GIVEAX(SCTV4,T≠F∧T≠UU∧F≠UU);
02600	
02700	GIVEAX(SCTV5,¬ββ(T,RTV,F) ∧ ¬ββ(F,RTV,T));
02800	
02900	GIVEAX(LIFTING,(∀ F)(∀ G)(∀ R1)(∀ R2)(SCORDERING R1 ∧ SCORDERING R2
03000	∧ FεDOMAIN(R1→→R2) ∧ GεDOMAIN(R1→→R2)
03100			⊃
03200	ββ(F,(R1→→R2),G)≡(∀ X)(XεDOMAIN R1 ⊃ ββ(β(F,X),R2,β(G,X)))));
03300	
03400	GIVEAX(KCOMB,(∀ R1)(∀ R2)(SCORDERING R1 ∧ SCORDERING R2
03500	⊃ KCOMB(R1,R2)εDOMAIN(R1→→(R2→→R1)) ∧ (∀ X)(∀ Y)(XεDOMAIN R1 ∧
03600	YεDOMAIN R2 ⊃ β(β(K(R1,R2),X),Y) = X)));
03700	
03800	GIVEAX(SCOMB,(∀ R1)(∀ R2)(∀ R3)(SCORDERING R1 ∧ SCORDERING R2
03900		∧ SCORDERING R3
04000				⊃
04100		SCOMB(R1,R2,R3) ε DOMAIN((R1→→(R2→→R3))→→((R1→→R2)→→R3))
04200		∧ (∀ F)(∀ G)(∀ X)(FεDOMAIN(R1→→(R2→→R3))
04300			∧ GεDOMAIN(R1→→R2)
04400			∧ X ε DOMAIN R1
04500				⊃
04600			β(β(β(SCOMB(R1,R2,R3),F),G),X) = β(F,β(G,X)))));
04700	
04800	GIVEAX(YCOMB,(∀ R)(SCORDERING R ⊃ YCOMB(R)ε DOMAIN((R→→R)→→R)
04900	∧ (∀ F)(FεDOMAIN(R→→R) ⊃ β(F,β(YCOMB(R),F))=F ∧
05000	(∀ G)(GεDOMAIN R ∧ β(F,G)=F ⊃ ββ(β(YCOMB R,F),R,G)))));
05100	
05200	GIVEAX(CCOMB,(∀ R1)(∀ R2)(SCORDERING R1 ∧ SCORDERING R2
05300	⊃CCOMB(R1,R2)εDOMAIN((R1→→RTV)→→((R1→→R2)→→((R1→→R2)→→(R1→→R2))))
05400	∧(∀ P)(∀ X)(∀ Y)(∀ U)(PεDOMAIN(R1→→RTV) ∧ XεDOMAIN(R1→→R2) ∧
05500	YεDOMAIN(R1→→R2) ∧ UεDOMAIN R1 ⊃ β(β(β(β(CCOMB(R1,R2),P),X),Y),U)
05600	= IF β(P,U)=UU THEN UU ELSE (IF β(P,U)=T THEN β(X,U) ELSE β(Y,U)))));
05700	
05800	GIVEAX(SCINDUCTION,(∀ R)(∀ F)(∀ P)(SCORDERING R ∧ FεDOMAIN(R→→R)
05900	∧ Pε(DOMAIN R→TV) ∧AIW(P,R) ∧ β(P,UU)=T
06000	∧ (∀ X)(XεDOMAIN R ∧ β(P,X)=T ⊃ β(P,β(F,X))=T)
06100	⊃β(P,β(YCOMB(R),F))=T));
06200	
06300	GIVEAX(EXT1,(∀ U)(ISSET U ∧ ¬(UUεU) ⊃ SCORDERING TORD U
06400		∧ DOMAIN TORD U = U ∪ UNITSET UU
06500		∧ (∀ X)(∀ Y)(X ε DOMAIN TORD U ∧ Y ε DOMAIN TORD U
06600		∧ ββ(X,TORD U,Y) ≡ X=UU ∧ YεU)));
06700	
06800	GIVEAX(EXT2,(∀ F)(∀ R)(ISMAP F ∧ ¬(UU ε DOMAIN F)
06900		∧ SCORDERING R ∧ RANGE F ⊂ DOMAIN R
07000				⊃
07100		EXT F ε DOMAIN(TORD DOMAIN F →→ R) ∧ β(EXT F,UU) = UU
07200		∧ (∀ X)(X ε DOMAIN F ⊃ β(EXT F,X) = β(F,X))));
     

00100	END;